Inference at * 1 1 1 
Iof proof for Lemma equiv rel functionality wrt iff:



1. T : Type
2. T' : Type
3. E : TT
4. E' : T'T'
5. T = T'
6. x, y:T. E(x,y)  E'(x,y)
  ((a:T. E'(a,a)) & (a, b:T. E'(a,b)  E'(b,a)) & (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c)))
   ((a:T'. E'(a,a))
   & (a, b:T'. E'(a,b)  E'(b,a))
   & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c))) 

latex

 by AssertLemma `equiv_rel_iff` [] 

latex

 1: 

 1: 7. EquivRel(;A,B.A  B)
 1:   ((a:T. E'(a,a))
 1:   & (a, b:T. E'(a,b)  E'(b,a))
 1:   & (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c)))
 1:    ((a:T'. E'(a,a))
 1:    & (a, b:T'. E'(a,b)  E'(b,a))
 1:    & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
 .

Lemmas

equiv rel iff